$\forall$$T$:Type, $l$:$T$ List, $P$:($T$$\rightarrow$Prop), $a$, $x$:$T$.
\\[0ex]$y$ = succ($x$) in $a$.$l$
\\[0ex]$\Rightarrow$ $P$($y$)
\\[0ex]$\Rightarrow$ ($x$ $=$ $a$ $\Rightarrow$ 0$<\parallel$$l$$\parallel$ $\Rightarrow$ $P$(hd($l$))) \& ($\neg$$x$ $=$ $a$ $\Rightarrow$ $y$ = succ($x$) in $l$$\Rightarrow$ $P$($y$))